﻿namespace LambdaCalc.Spike

open System

type Identifier = string

type Term =
    | Id of Identifier
    | App of Term*Term
    | Lambda of Identifier*Term
    with
    member t.ToFormula() =
        match t with
        | Id s -> s
        | App (t1,t2) -> sprintf "%s %s" (t1.ToFormula()) (t2.ToFormula())
        | Lambda (x,r) -> sprintf "\\lambda %s.(%s)" x (r.ToFormula())
    override t.ToString() =
        match t with
        | Id s -> s
        | App (t1,t2) -> sprintf "(%s %s)" (t1.ToString()) (t2.ToString())
        | Lambda (x,r) -> sprintf "\\%s.%s" x (r.ToString())
    static member Parse(text : string) =
        let index = ref 0
        let step() = incr index
        let rec parseMain () =
            match text.[!index] with
            | '\\' -> parseLambda()
            | '(' -> parseApp()
            | _ -> parseId()
        and parseName() = 
            let rec parseString r =
                if !index + r >= text.Length then r else
                if Char.IsLetterOrDigit (text, !index+r)
                then parseString (r+1)
                else r
            let len = parseString 0
            let res = text.Substring(!index, len)
            index := !index + len
            res
        and parseId () =
            Id <| parseName()
        and parseApp() =
            step()
            let first = parseMain ()
            parseLeer()
            let second = parseMain ()
            parseKlammerZu()
            App (first, second)
        and parseLambda() =
            step()
            let id = parseName()
            parsePoint()
            let rest = parseMain()
            Lambda (id, rest)
        and parseLeer() =
            match text.[!index] with
            | ' ' -> step()
            | _   -> failwith "<space> erwartet"
        and parsePoint() =
            match text.[!index] with
            | '.' -> step()
            | _   -> failwith ". erwartet"
        and parseKlammerZu() =
            match text.[!index] with
            | ')' -> step()
            | _   -> failwith ") erwartet"
        parseMain()